\begin{tabbing}
$\forall$\=${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), ${\it Aa}$, ${\it Ba}$, ${\it Ab}$, ${\it Bb}$:Type, ${\it Ca}$:Component(${\it ds}$;${\it da}$;${\it Aa}$;${\it Ba}$),\+
\\[0ex]${\it Cb}$:Component(${\it ds}$;${\it da}$;${\it Ab}$;${\it Bb}$), ${\it Pa}$:ComponentSpec(${\it Aa}$;${\it Ba}$), ${\it Pb}$:ComponentSpec(${\it Ab}$;${\it Bb}$).
\-\\[0ex]component{-}compatible(${\it ds}$;${\it da}$;${\it Aa}$;${\it Ab}$;${\it Ca}$;${\it Cb}$)
\\[0ex]$\Rightarrow$ component{-}output{-}disjoint\{i:l\}(${\it ds}$;${\it da}$;${\it Aa}$;${\it Ab}$;${\it Ca}$;${\it Cb}$)
\\[0ex]$\Rightarrow$ ${\it Ca}$ $\mid${-} ${\it es}$,${\it in}$,${\it out}$.${\it Pa}$(${\it es}$,${\it in}$,${\it out}$)
\\[0ex]$\Rightarrow$ ${\it Cb}$ $\mid${-} ${\it es}$,${\it in}$,${\it out}$.${\it Pb}$(${\it es}$,${\it in}$,${\it out}$)
\\[0ex]$\Rightarrow$ mux{-}component(${\it Ca}$;${\it Cb}$) $\mid${-} ${\it es}$,${\it in}$,${\it out}$.\=${\it Pa}$(${\it es}$,es{-}interface{-}left(${\it in}$),es{-}interface{-}left(${\it out}$))\+
\\[0ex]\& ${\it Pb}$\=(${\it es}$\+
\\[0ex],es{-}interface{-}right(${\it in}$)
\\[0ex],es{-}interface{-}right(${\it out}$))
\-\-
\end{tabbing}